Operation of the Proof Checker

			Whitfield Diffie


			Introduction

	The  program  `PCHECK'  is  a  proof  checker  for  a natural
deduction formulation of the first  order  predicate  calculus.    It
performs the function of a logical adding machine, aiding the user in
handling large formal proofs.   The system has the ability to manage
a  working  set of logical data upon which it will perform inferences
in response to user commands.

	The  four major kinds of objects with which the proof checker
deals are axioms, schemas, proofs and theorems.   Each  of  these  is
the fraternal, if not the identical, twin of its namesake in ordinary
informal mathematics. Every object has a name which is  used  by  any
command  refering  to  it.  These things are described briefly in the
paragraphs below.

	Axioms are logical propositions of arbitrary character  which
may  be  added  by  the  user  at  any time.   The program imposes no
standards on the set of axioms.

	Schemas are propositions depending on a functional  variable,
for  which  a  function or predicate may be instantiated.  Only axiom
schemas are available at present.

	Proofs are the principle objects of  interest  in  the  proof
checker.   Each  proof consists of a sequence of lines, each of which
follows from some  or  all  of  the  lines  above  it.    A  line  is
identified  by  a  number  which is used in all references to it.  In
addition to its number, a line contains three items. The first is the
proposition  which  it asserts.  The second is the justification; the
inference rule which gave rise to the line.  The last is the list  of
assumptions on which it depends.

	Theorems are propositions which have been established through
proofs.  Any line of a proof  which  is  free  of  assumptions  is  a
potential  theorem  and may be declared so by the user.  A theorem is
stored under its name and may be used in the same way as an axiom.


	Most of the proof checker commands fall naturally into one of
two categories.    The first deals with the management of the  user's
working set as a whole.    It includes commands for taking inventory,
selecting or displaying  proofs,  and  communicating  with  secondary
storage.   The other contains those commands which implement rules of
inference.    These must be applied within the context of a  specific
proof,  giving  their  results as new proof lines.   Introduction and
elimination rules for each of the  logical  connectives,  along  with
specialization  an generalization rules for the quantifiers, and some
ad hoc rules for special cases are provided.


			Summary of Commands by Classes

A. Commands Which Implement Inference Rules

	AE		And elimination
	AI		And introduction
	ALT		Alternatives
	ASS		Assumption
	BS		Bound variable Substitution
	DED		Deduction
	DEF		Definition
	DNE		Double Negation Elimination
	DNI		Double Negation Introduction
	EG		Existential Generalization
	ELIM		Elimination
	EQE		Equivalence Elimination
	EQI		Equivalence Introduction
	ES		Existential Specialization
	IFE		If-Then-Else elimination
	IFI		If-Then-Else Introduction
	LC		Lambda Conversion
	NE		Negation Elimination
	NI		Negation Introduction
	OE		Or Elimination
	OI		Or Introduction
	REP		Replacement
	REPL		Replace Left Side
	REPR		Replace Right Side
	TAUT		Tautology
	UG		Universal Generalization
	US		Universal Specialization
	USEAX		Use Axiom
	USESCHEMA	Use Schema
	USETHM		Use Theorem


B. Commands Which Do Other Useful Things

	BT		Back To
	FINDL		Find Lines
	GIVEAX		Give Axiom
	GIVESCHEMA	Give Schema
	INVENTORY	Inventory
	MAKETHM		Make Theorem
	ONDD		On Data Disk Display
	ONIII		On III Display
	ONTTY		On Teletype
	PROOF		Proof
	REDO		Redo
	RESTOREALL	Restore All
	SAVEALL		Save All
	SAVECOMS	Save Commands
	SHOW		Show
	SHOWALL		Show All
	SSEX		Show S-expressions


			Syntax and Abbreviations

Biconditional:	A EQUIVALENT B	or	A EQU B	or	A≡B
Conjunction:	A AND B	or	A ∧ B	or	A & B
Disjunction:	A OR B	or	A ∨ B
Negation:	NOT A	or	¬ A
Implication:	A IMPLIES B or	A IMP B	or	A ⊃ B	or	A=>B
Universal Quantification:	(FORALL X)---	or (ALL X)---
				or	(∀ x)---
Existential Quantification:	(THEREEXISTS X)---	or (EXISTS X)---
				or	(∃ x)---
	The most recent line of proof is represented by "@."


			Availability

	The source program is called PCHECK and resides on  the  disk
area  [CHE,WD].    It will usually be available as a dumped copy with
the name PCHECK.DMP, on the system area [1,3]. To use this copy it is
only  necessary  to  type  `R PCHECK <cr>.' It will respond by typing
`PROOF-CHECKER,' at this point  one  is  conversing  with  the  proof
checker and may use its commands.


			Examples

	There follow two delightful examples of the  proof  checker's
operation  on  simple  problems.   The user's sentiments begin at the
left margin, while the program's responses are  indented  by  one  or
more tabs.

PROOF ONE;
	PROOF ONE

ASS(P⊃(Q⊃R));
	1:	P⊃Q⊃R BY ASSUMPTION 
ASS(P⊃Q);
	2:	P⊃Q BY ASSUMPTION 
ASS P;
	3:	P BY ASSUMPTION 
MP(2,3);
	4:	Q BY MP(2,3) ASSUMING (2 3) 
MP(1,3);
	5:	Q⊃R BY MP(1,3) ASSUMING (1 3) 
MP(4,5);
	6:	R BY MP(4,5) ASSUMING (2 1 3) 
DED(6,3);
	7:	P⊃R BY DED(6,3) ASSUMING (2 1) 
DED(7,2);
	8:	(P⊃Q)⊃P⊃R BY DED(7,2) ASSUMING (1) 
DED(8,1);
	9:	(P⊃Q⊃R)⊃(P⊃Q)⊃P⊃R BY DED(8,1) ASSUMING NIL 


PROOF TWO;
	PROOF TWO

ASS((∃ Y) ((∀ X) F(X,Y)));
	1:	(∃ Y) (∀ X) F(X,Y) BY ASSUMPTION 
ES(1,A);
	2:	(∀ X) F(X,A) BY ES(1,A) ASSUMING (1) 
US(2,X);
	3:	F(X,A) BY US(2,X) ASSUMING (1) 
EG(3,A,Y);
	4:	(∃ Y) F(X,Y) BY EG(3,A,Y) ASSUMING (1) 
UG(4,X);
	5:	(∀ X) (∃ Y) F(X,Y) BY UG(4,X) ASSUMING (1) 
DED(5,1);
	6:	(∃ Y) (∀ X) F(X,Y)⊃(∀ X) (∃ Y) F(X,Y) BY DED(5,1) ASSUMING NIL 

	In each case the last line represents the theorem to be proved.


			Commands

AndElemination(line,choices)	P1 ∧ P2 ∧ ... ∧ Pn
 				------------------
				   Pj ∧ ... ∧ pk

	The first argument is the line to which the  rule  is  to  be
applied  and  the  rest  are the numbers of the chosen conjuncts. The
result is the conjunction of thoese conjuncts chosen.

AndIntroduction(Line1,Line2,Line3...)	P , Q , R ...
					-------------
					P ∧ Q ∧ R ...

	This command goes from lines with propositions P,Q,R etc.  to
a  line  with  the  conjunction  of  these  propostions.  Its  set of
assumptions is the union of those of its arguments.

ALTernatives(line1,line2)   A⊃B,¬A⊃B	(order doesn't matter)
			    --------
			        B

	Alt goes from two proofs  of  the  same  fact  starting  with
contradictory  assumptions  to  the  conclusion  of  the fact without
assumptions.

ASSume(PROPOSITION)
	This  command  introduces  a  line  of  proof representing an
assumption.  It's set of assumptions contains only itself.

BoundSubstitution(line,..pairs..)

	This command changes the bound variebles of a  formula.   The
latter arguments are dotted pairs of identifiers, of which the second
is  substituted  for  the  first.   All  substitutions   take   place
simultaneously.


BackTo(stepno)

	If  this  command  has no argument, it backs the proof up one
step, otherwise it backs it up to the stepnumber given.

DEDuce(conclusion,premises)	B , A		B , A1 , A2 ...
				-----	or	---------------
				A ⊃ B		 A1∧A2∧... ⊃ B

	The  first argument of this command is the line number of the
conclusion and the rest are the line numbers of the premises if  any.
If  there are no premises the result will have the form `True ⊃ ...,'
if there is one premise `A' it will have the form `A⊃...,'  if  there
are several eg. `A, B, C' then it will have the form `A∧B∧C⊃....' The
assumptions of the resulting line are those of the  conclusion  minus
the line numbers of the premises.

DEFinition(name,expression)

	The resulting line behaves in all respects  like  an  assumed
equality statement, except that it may be eliminated as an assumption
by the ELIMinate command which will  remove  all  occurrences  of the
name.

DoubleNegationElimination(line)		¬¬A
					---
					 A

	The argument is the line number of a  proposition  of  double
negative  form  and  the  result  is  a  new  line with the negatives
removed.

DoubleNegationIntroduction(line)	 A
					---
					¬¬A

	The argument is any line and  the  result  is  a  line  whose
propostion is the same with two negatives added.

ELIMination(line,definition)

	This does a replacement of all occurrences of the  left  side
of the definition by the right in the line and removes the definition
from the assumption list of the result.


EQuivalenceElimination(line.choice)	A≡B		A≡B
					---	or	---
					A⊃B		B⊃A

	The first argument is the number  of  a  line  containing  an
equivalence(biconditional), and the  second is a number telling which
half is wanted.  A value of one indicates the first half is required,
while two indicates the second half.  The result is a line containing 
an implication.

EQuivalenceIntroduction(line1,line2)	A⊃B,B⊃A
					-------
					  A≡B

	The  arguments  are  the numbers of lines containing converse
implications.  The result is a new line containing a biconditional.

ExistentialGeneralization(line,O1.N1...)	  formula in O1,...
						--------------------
						(∃ N1) formula in N1

	Surrounds a formula with existential quantifiers  subject  to
the  usual  restrictions.   The  first argument is a line number, and
each of the others may be either a single variable or a dotted  pair.
In  the  latter  case, the second element of the pair will be used as
the bound variable if this is permissible.

ExistentialSpecialization(line,newname)		∃x A
						----
						  x
						 A
						  newname

	The  first  argument  is  the  number of a line containing an
existentially quantified proposition, and the  second  is  an  unused
constant  name.  The result is a line with the quantifier removed and
the name substituted for all occurrences of the quantified variable.


FINDLines(formula,proof)
	This  command  searches  the  lines  of a proof for the lines
containing a given formula, printing each one as it is encountered.

GIVEAXiom(name,prop)

	The proposition is taken as an axiom and may be  referred  to
by name.

GIVESCHEMA(name,schema)

	This  behaves  like the above, except that the schema must be
specified in the rather complicated form:
	`(PRED letter)(...form using the predicate letter...)'. 
The Induction schema is supplied with the system.

INVENTORY()
	This command prints a table showing all axioms, theorems, and
proofs.

IFElimination(line1,line2)
			A,IF A THEN B ELSE C	¬A,IF A THEN B ELSE C
			-------------------- or	--------------------
				B			C

	The   arguments   are   lines  containing  an  "IF-THEN-ELSE"
statement and either the conditional predicate or its  negation.  The
result  is  a line with either the "THEN" clause or the "ELSE" clause
respectively. The order of the arguments does not matter.

IFIntroduction(line1,line2)	     A⊃B,¬A⊃C
				------------------
				IF A THEN B ELSE C

	The arguments are lines containing suitable implications  and
the  result  is a line containing an "IF-THEN-ELSE" statement derived
from them.  The order of the arguments does not matter.

LambdaConvert(lamexp,arg)

	Produces an equality line with the  original  application  of
the  lambda expression to its arguments on the left, and the expanded
form with the argument substituted for the variable on the right.


MAKETHeoreM(name,line)
	The  arguments  are  a name and a the number of a line in the
current proof.  The line must have no assumptions.

ModusPonens(line1,line2)	A,A⊃B		A⊃B,A
				-----	or	-----
				  B		  B

	If  the  arguments  of  this command are the numbers of lines
whose propositions are of the forms "P" and "P ⊃ Q" then  the  result
will be a line with the propostion "Q." The assumptions are the union
of the assumptions of the parent lines.  The order of  the  arguments
does not matter.

NotElimination(line1,line2)	A , ¬A		¬A , A
				------	or	------
				FALSE		FALSE

	The arguments are the numbers of lines, one of which contains
proposition and the other of which contains its negation.  The result
is a line containing the logical constant FALSE.

NotIntroduction(line)	A ⊃ FALSE
			---------
			   ¬A

	The  argument is the number of a line of the form, "something
IMPLIES FALSE" and the  result  is  a  new  line  of  the  form  "Not
something."


ONDD()		for Data Disk Display
ONIII()		for III Display
ONTTY()		for Teletype

	These commands are not specific to any proof and may be given
at any time.   They initialize the output for the character  set  and
pagewidth of the various available terminals.

OrElimination(or,imp1,...)	P1∨P2∨...∨Pn,P1⊃Q,P2⊃Q,...,Pn⊃Q
				-------------------------------
					       Q

	The  first  argument  is  a  disjunction  and  the  rest  are
implications each with the same consequent and one of  the  disjuncts
as antecedent.   The result is a line containing the consequent.

OrIntroduction(prop1,prop2,...)		P , Q , ...
					-----------
					P ∨ Q ∨ ...

	The arguments of this command may be either line  numbers  or
propositions,  includeing  at least one line number.  The result is a
line  containing  the  disjunction  of  the  propositions  given  and
depending on the assumptions of any lines mentioned.

PROOF(name)
	
	This  command  initializes  a  proof.   If  it  is  given  an
indentifier as an argument, the proof will have  that  as  its  name,
otherwise  a name of the form "PROOFn" will be assigned. If the proof
named already exists it will be resumed. In all cases the proof named
becomes the subject of the program's attention.

REDO(oldline,newline)
	This  command  corresponds  to  that  situation where one has
shown a result by making an assumption and now wishes to conclude the
proof  by  proving  the assumption.  The arguments are the numbers of
lines whose propositions must be the same. The second will  be  taken
in  place  of  the  first and all lines of the proof depending on the
first will be recalculated and added to the end.  In general this may
add  many  lines to the proof and will end with a line similar to the
previous last line except for the removal of some assumptions.


REPlace(any line,equality line,left or right flag)

	The second argument is the number of a line with an  equality
statement  and the first is the number of any line of the proof.  the
third is a flag which if 1 causes the right  half  of  the  first  to
replace  the  left  in  the  second line, and if 2 causes the left to
replace the right.

REPlaceLeft(line,equality,number)
	This command replaces the left  side  of  "equality"  by  the
right side in "line" only at the occurrence indicated by the number.

REPlaceRight(line,equality,number)
	This command replaces the right side  of  "equality"  by  the
left side in "line" only at the occurrence indicated by the number.


RESTOREALL(filename)

	If no file name is given then the  file  "INIT.PRF"  will  be
loaded.  Otherwise it will be the file named.

SAVEALL(filename)

	This command saves the state of the  world  in  a  form  more
compact  than a dump file.  If no argument is given, it will create a
file called "INIT.PRF" which will automatically  be  loaded  whenever
the  proofchecker  is started by this user.  If an argument is given,
it will be taken as a filename.  Material saved under explicit  names
is  not  automatically  loaded,  but  must be loaded with the command
"RESTOREALL."

SAVECOMS(filename)

	This command writes out a file with the given name containing
commands  which  will reproduce the present environment when reloaded
with `RESTOREALL'. Since this forces the proof to be re-checked, upon
reloading, this file may be edited legitimately.

SHOW(names of devices, axioms, proofs etc. or line numbers)
	This command displays axioms, proofs etc. If no arguments are
given then the current proof will be  shown.    If  it  is  given  as
arguments the names of axioms, proofs etc. these will be displayed on
the terminal.  If one of the arguments is a device name, ie. a quoted
expression  of  the  form  '(DSK:   FOO),  then  the  output from the
following arguments will be directed to that device.  Finally, if  an
argument  is  or a consecutive pair of arguments are numbers then the
corresponding line or range  will  be  shown.     In  short  it  does
everything.

SHOWALL(file and device names)
	This command displayes all proofs, axioms etc. in the system.
If a filename is given it will be used, otherwise printing will be on
the console.

SSEX(name)
	This command is used for debugging.  It displays one proof in
much the same manner as show except that is shows the S-expression to
permit debugging of syntax parsing errors. If no argument is given it
displays the current proof otherwise the proof named.

TAUTology(conclusion,supporting lines)

	This   rule   performs  any  inference  which  is  of  purely
propositional character.  Its first argument is the formula  desired,
and  the  remaining  arguments  are  the  numbers of lines containing
supporting propositions.


UniversalGeneralization(line,O1.N1,...)       "expression in O1,..."
					    -------------------------
					    (∀ N1) "expression in N1"

	The  first  argument  must  be  a  line number.  The rest are
either variables to be generalized or dotted pairs of same  with  new
names to be used as bound variables in the quantified expression.  If
the new variables are supplied they will  be  checked  for  propriety
before acceptance.

UniversalSpecialization(line,term)	(∀ x)"expression in X"
					----------------------
					 "expression in term"

	The first argument is the  number  of  a  line  containing  a
universal  generalization, and the second is a term to be substituted
for the bound variable of the universal quantifier. The result  is  a
line  containing  a  specific instance of the generalization in which
the term has been substituted for all appropriate occurrences  of the
variable.   If  necessary,  the names of other bound variables in the
universal expression will be changed to avoid conflict with the  free
variables of the term.

USEAXiom(name,..terms..)

	Leading quantifiers in the named axiom will be specialized to
the  terms  given  and  the  result  will become a line of the proof,
depending on no assumptions.

USETHeoreM(name)

	Leading  quantifiers in the named theorem will be specialized
to the terms given and the result will become a line  of  the  proof,
depending on no assumptions.

USESCHEMA(schema,predicate)

	The  first argument is the name of a schema and the second is
either a predicate letter  or  a  lambda  expression  which  will  be
substituted  in  the  schema  for its predicate variable.  The result
will become the next line of the proof.


			APPENDIX
				John McCarthy

	This appendix documents a collection of commands  for  PCHECK
which  generate  assertions about S-expressions.  As it happens, none
of the commands are  rules  of  inference  in  the  sense  of  taking
previous  sentences  as premises.   They are rather axiom generators.


EValuateCAR(s-expression)
	If the argument is not a quoted S-expression, no new line  is
generated.     If  the  argument  is  a  quoted  atom,  then  a  line
s-expression=UU is generated.  If the argument is a quoted non-atomic
S-expression,  then  a  line  CAR(s-expression)='car[s-expression] is
generated.  Thus, EVCAR(A) produces  no  result,  EVCAR('A)  produces
CAR('A)=UU and EVCAR('(A B)) produces CAR('(A B))='A.

EValuateCDR(s-expression)
	EVCDR is similar to EVCAR with the obvious difference.

EValuateCONS(sexp1,sexp2)
	If  not both sexp1 and sexp2 are quoted S-expressions, EVCONS
does nothing.   Otherwise,  it  generates  a  sentence  of  the  form
CONS(sexp1,sexp2)=cons[sexp1,sexp2].     Thus EVCONS('A,'B) generates
CONS('A,'B)='(A.B).

EValuateEQUAL(sexp1,sexp2)
	EVEQUAL(sexp1,sexp2)  asserts  the  equality or inequality of
two quoted S-expressions.  Thus EVEQUAL('(A B),'(A B)) generates  '(A
B)='(A B) and EVEQUAL('A,'B) generates ¬('A='B).

EValuateATOM(sexp)
	EVATOM(sexp) tells us whether  sexp  is  atomic.   EVATOM('A)
generates ATOM('A) and EVATOM('(A B)) generates ¬ATOM('(A B)).


ISSEXPression(sexp)
	ISSEXP(sexp) asserts that its argument is an S-expression  if
it  is  a  quoted S-expression.  Thus ISSEXP('A) generates ISSEXP('A)
while ISSEXP(A) does not generated a line since the value of A may or
may not be an S-expression.

EValuateLIST(list of quoted S-expressions)
	EVLIST(list  of  quoted S-expressions) generates an assertion
that the list of the expressions has its value.   Thus  EVLIST('A,'(A
B),'C) generates LIST('A,'(A B),'C)='(A (A B) C).

EValuateEVAL(sexp)
	EVEVAL(sexp)  generates  an assertion that EVAL(sexp) has the
value given it by the LISP evaluator.  A censor is supposed to  check
that the evaluation of sexp involves only pure LISP functions and not
any pseudo-functions with side  effects  like  SETQ's  and  RPLACA's.
However,  the censor isn't working yet.  Thus EVEVAL('(CADR (QUOTE (A
B))) generates EVAL('(CADR (QUOTE (A B)))='B.

INTegerQUOTE(integer)
	INTQUOTE(integer) generates  an  assertion  that  integer  is
equal to the integer quoted.  This gets around the fact that integers
unlike  other  atoms  in  LISP  don't  have  to  be  quoted.     Thus
NTQUOTE(27) generates	27='27.   Needless  to say, INTQUOTE balks at
non-integer arguments.

ISINTeger(integer)
	ISINT(integer)  generates  an  assertion  that  the  argument
belongs  to  the  set  of  integers  if  this  is so.  Thus ISINT(27)
generates 27εI, and ISINT(A) generates an error message.